${\it pr}$ implements ${\it kpr}$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$K{-}sem($S$;${\it equiv}$)(${\it kpr}$,$S$(${\it pr}$))